Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		le(0,Y)	→ true
2:		le(s(X),0)	→ false
3:		le(s(X),s(Y))	→ le(X,Y)
4:		minus(0,Y)	→ 0
5:		minus(s(X),Y)	→ ifMinus(le(s(X),Y),s(X),Y)
6:		ifMinus(true,s(X),Y)	→ 0
7:		ifMinus(false,s(X),Y)	→ s(minus(X,Y))
8:		quot(0,s(Y))	→ 0
9:		quot(s(X),s(Y))	→ s(quot(minus(X,Y),s(Y)))

There are 6 dependency pairs:


10:		LE(s(X),s(Y))	→ LE(X,Y)
11:		MINUS(s(X),Y)	→ IFMINUS(le(s(X),Y),s(X),Y)
12:		MINUS(s(X),Y)	→ LE(s(X),Y)
13:		IFMINUS(false,s(X),Y)	→ MINUS(X,Y)
14:		QUOT(s(X),s(Y))	→ QUOT(minus(X,Y),s(Y))
15:		QUOT(s(X),s(Y))	→ MINUS(X,Y)

The approximated dependency graph contains 3 SCCs: {10}, {11,13} and {14}.

Consider the SCC {10}. There are no usable rules. By taking the AF π with π(LE) = 1 together with the lexicographic path order with empty precedence, rule 10 is strictly decreasing.

Consider the SCC {11,13}. The usable rules are {1-3}. By taking the AF π with π(le) = π(MINUS) = 1 and π(IFMINUS) = 2 together with the lexicographic path order with precedence 0 ≻ true and s ≻ false, rule 11 is weakly decreasing and the rules in {1-3,13} are strictly decreasing.

Consider the SCC {14}. The usable rules are {1-7}. By taking the AF π with π(le) = π(minus) = π(QUOT) = 1 and π(ifMinus) = 2 together with the lexicographic path order with precedence s ≻ 0 ≻ true and s ≻ false, the rules in {4,5,7} are weakly decreasing and the rules in {1-3,6,14} are strictly decreasing.

Hence the TRS is terminating.

Tyrolean Termination Tool (0.16 seconds) --- May 3, 2006